(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Missing Ring›

text ‹This theory contains several lemmas which might be of interest to the Isabelle distribution.›

theory Missing_Ring
imports
  "HOL-Algebra.Ring"
begin

context comm_monoid
begin

lemma finprod_reindex_bij_betw: "bij_betw h S T 
  ⟹ g ∈ h ` S → carrier G 
  ⟹ finprod G (λx. g (h x)) S = finprod G g T"
  using finprod_reindex[of g h S] unfolding bij_betw_def by auto

lemma finprod_reindex_bij_witness:
  assumes witness:
    "⋀a. a ∈ S ⟹ i (j a) = a"
    "⋀a. a ∈ S ⟹ j a ∈ T"
    "⋀b. b ∈ T ⟹ j (i b) = b"
    "⋀b. b ∈ T ⟹ i b ∈ S"
  assumes eq:
    "⋀a. a ∈ S ⟹ h (j a) = g a"
  assumes g: "g ∈ S → carrier G"
  and h: "h ∈ j ` S → carrier G"
  shows "finprod G g S = finprod G h T"
proof -
  have b: "bij_betw j S T"
    using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
  have fp: "finprod G g S = finprod G (λx. h (j x)) S"
    by (rule finprod_cong, insert eq g, auto)
  show ?thesis
    using finprod_reindex_bij_betw[OF b h] unfolding fp .
qed
end

lemmas (in abelian_monoid) finsum_reindex_bij_witness = add.finprod_reindex_bij_witness

locale csemiring = semiring + comm_monoid R

context cring
begin
sublocale csemiring ..
end

lemma (in comm_monoid) finprod_one': 
  "(⋀ a. a ∈ A ⟹ f a = 𝟭) ⟹ finprod G f A = 𝟭"
  by (induct A rule: infinite_finite_induct, auto)

lemma (in comm_monoid) finprod_split: 
  "finite A ⟹ f ` A ⊆ carrier G ⟹ a ∈ A ⟹ finprod G f A = f a ⊗ finprod G f (A - {a})"
  by (rule trans[OF trans[OF _ finprod_Un_disjoint[of "{a}" "A - {a}" f]]], auto,
  rule arg_cong[of _ _ "finprod G f"], auto)

lemma (in comm_monoid) finprod_finprod:
  "finite A ⟹ finite B ⟹ (⋀ a b. a ∈ A  ⟹ b ∈ B ⟹ g a b ∈ carrier G) ⟹
  finprod G (λ a. finprod G (g a) B) A = finprod G (λ (a,b). g a b) (A × B)"
proof (induct A rule: finite_induct)
  case (insert a' A)
  note IH = this
  let ?l = "(⨂a∈insert a' A. finprod G (g a) B)"
  let ?r = "(⨂a∈insert a' A × B. case a of (a, b) ⇒ g a b)"
  have "?l = finprod G (g a') B ⊗ (⨂a∈A. finprod G (g a) B)"
    using IH by simp
  also have "(⨂a∈A. finprod G (g a) B) = finprod G (λ (a,b). g a b) (A × B)"
    by (rule IH(3), insert IH, auto)
  finally have idl: "?l = finprod G (g a') B ⊗ finprod G (λ (a,b). g a b) (A × B)" .
  from IH(2) have "insert a' A × B = {a'} × B ∪ A × B" by auto
  hence "?r = (⨂a∈{a'} × B ∪ A × B. case a of (a, b) ⇒ g a b)" by simp
  also have "… = (⨂a∈{a'} × B. case a of (a, b) ⇒ g a b) ⊗ (⨂a∈ A × B. case a of (a, b) ⇒ g a b)"
    by (rule finprod_Un_disjoint, insert IH, auto)
  also have "(⨂a∈{a'} × B. case a of (a, b) ⇒ g a b) = finprod G (g a') B"
    using IH(4) IH(5)
  proof (induct B rule: finite_induct)
    case (insert b' B)
    note IH = this
    have id: "(⨂a∈{a'} × B. case a of (a, b) ⇒ g a b) = finprod G (g a') B"
      by (rule IH(3)[OF IH(4)], auto)
    have id2: "⋀ x F. {a'} × insert x F = insert (a',x) ({a'} × F)" by auto
    have id3: "(⨂a∈insert (a', b') ({a'} × B). case a of (a, b) ⇒ g a b)
      = g a' b' ⊗ (⨂a∈({a'} × B). case a of (a, b) ⇒ g a b)"
      by (rule trans[OF finprod_insert], insert IH, auto)
    show ?case unfolding id2 id3 id
      by (rule sym, rule finprod_insert, insert IH, auto)
  qed simp
  finally have idr: "?r = finprod G (g a') B ⊗ (⨂a∈A × B. case a of (a, b) ⇒ g a b)" .
  show ?case unfolding idl idr ..
qed simp

lemma (in comm_monoid) finprod_swap:
  assumes "finite A" "finite B" "⋀ a b. a ∈ A  ⟹ b ∈ B ⟹ g a b ∈ carrier G"
  shows "finprod G (λ (b,a). g a b) (B × A) = finprod G (λ (a,b). g a b) (A × B)"
proof -
  have [simp]: "(λ(a, b). (b, a)) ` (A × B) = B × A" by auto
  have [simp]: "(λ x. case case x of (a, b) ⇒ (b, a) of (a, b) ⇒ g b a) = (λ (a,b). g a b)"
    by (intro ext, auto)
  show ?thesis 
    by (rule trans[OF trans[OF _ finprod_reindex[of "λ (a,b). g b a" "λ (a,b). (b,a)"]]],
    insert assms, auto simp: inj_on_def)
qed

lemma (in comm_monoid) finprod_finprod_swap:
  "finite A ⟹ finite B ⟹ (⋀ a b. a ∈ A  ⟹ b ∈ B ⟹ g a b ∈ carrier G) ⟹
  finprod G (λ a. finprod G (g a) B) A = finprod G (λ b. finprod G (λ a. g a b) A) B"
  using finprod_finprod[of A B] finprod_finprod[of B A] finprod_swap[of A B]
  by simp



lemmas (in semiring) finsum_zero' = add.finprod_one' 
lemmas (in semiring) finsum_split = add.finprod_split 
lemmas (in semiring) finsum_finsum_swap = add.finprod_finprod_swap


lemma (in csemiring) finprod_zero: 
  "finite A ⟹ f ∈ A → carrier R ⟹ ∃a∈A. f a = 𝟬
   ⟹ finprod R f A = 𝟬"
proof (induct A rule: finite_induct)
  case (insert a A)
  from finprod_insert[OF insert(1-2), of f] insert(4)
  have ins: "finprod R f (insert a A) = f a ⊗ finprod R f A" by simp
  have fA: "finprod R f A ∈ carrier R"
    by (rule finprod_closed, insert insert, auto)
  show ?case
  proof (cases "f a = 𝟬")
    case True
    with fA show ?thesis unfolding ins by simp
  next
    case False
    with insert(5) have "∃ a ∈ A. f a = 𝟬" by auto
    from insert(3)[OF _ this] insert have "finprod R f A = 𝟬" by auto
    with insert show ?thesis unfolding ins by auto
  qed
qed simp

lemma (in semiring) finsum_product:
  assumes A: "finite A" and B: "finite B"
  and f: "f ∈ A → carrier R" and g: "g ∈ B → carrier R" 
  shows "finsum R f A ⊗ finsum R g B = (⨁i∈A. ⨁j∈B. f i ⊗ g j)"
  unfolding finsum_ldistr[OF A finsum_closed[OF g] f]
proof (rule finsum_cong'[OF refl])
  fix a
  assume a: "a ∈ A"
  show "f a ⊗ finsum R g B = (⨁j∈B. f a ⊗ g j)"
  by (rule finsum_rdistr[OF B _ g], insert a f, auto)
qed (insert f g B, auto intro: finsum_closed)
    
lemma (in semiring) Units_one_side_I: 
  "a ∈ carrier R ⟹ p ∈ Units R ⟹ p ⊗ a = 𝟭 ⟹ a ∈ Units R"
  "a ∈ carrier R ⟹ p ∈ Units R ⟹ a ⊗ p = 𝟭 ⟹ a ∈ Units R"
  by (metis Units_closed Units_inv_Units Units_l_inv inv_unique)+

context ordered_cancel_semiring begin
subclass ordered_cancel_ab_semigroup_add ..
end

text ‹partially ordered variant›
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
  assumes mult_strict_left_mono: "a < b ⟹ 0 < c ⟹ c * a < c * b"
  assumes mult_strict_right_mono: "a < b ⟹ 0 < c ⟹ a * c < b * c"
begin

subclass semiring_0_cancel ..

subclass ordered_semiring
proof
  fix a b c :: 'a
  assume A: "a ≤ b" "0 ≤ c"
  from A show "c * a ≤ c * b"
    unfolding le_less
    using mult_strict_left_mono by (cases "c = 0") auto
  from A show "a * c ≤ b * c"
    unfolding le_less
    using mult_strict_right_mono by (cases "c = 0") auto
qed

lemma mult_pos_pos[simp]: "0 < a ⟹ 0 < b ⟹ 0 < a * b"
using mult_strict_left_mono [of 0 b a] by simp

lemma mult_pos_neg: "0 < a ⟹ b < 0 ⟹ a * b < 0"
using mult_strict_left_mono [of b 0 a] by simp

lemma mult_neg_pos: "a < 0 ⟹ 0 < b ⟹ a * b < 0"
using mult_strict_right_mono [of a 0 b] by simp

text ‹Legacy - use ‹mult_neg_pos››
lemma mult_pos_neg2: "0 < a ⟹ b < 0 ⟹ b * a < 0" 
by (drule mult_strict_right_mono [of b 0], auto)

text‹Strict monotonicity in both arguments›
lemma mult_strict_mono:
  assumes "a < b" and "c < d" and "0 < b" and "0 ≤ c"
  shows "a * c < b * d"
  using assms apply (cases "c=0")
  apply (simp)
  apply (erule mult_strict_right_mono [THEN less_trans])
  apply (force simp add: le_less)
  apply (erule mult_strict_left_mono, assumption)
  done

text‹This weaker variant has more natural premises›
lemma mult_strict_mono':
  assumes "a < b" and "c < d" and "0 ≤ a" and "0 ≤ c"
  shows "a * c < b * d"
by (rule mult_strict_mono) (insert assms, auto)

lemma mult_less_le_imp_less:
  assumes "a < b" and "c ≤ d" and "0 ≤ a" and "0 < c"
  shows "a * c < b * d"
  using assms apply (subgoal_tac "a * c < b * c")
  apply (erule less_le_trans)
  apply (erule mult_left_mono)
  apply simp
  apply (erule mult_strict_right_mono)
  apply assumption
  done

lemma mult_le_less_imp_less:
  assumes "a ≤ b" and "c < d" and "0 < a" and "0 ≤ c"
  shows "a * c < b * d"
  using assms apply (subgoal_tac "a * c ≤ b * c")
  apply (erule le_less_trans)
  apply (erule mult_strict_left_mono)
  apply simp
  apply (erule mult_right_mono)
  apply simp
  done

end

class ordered_idom = idom + ordered_semiring_strict +
  assumes zero_less_one [simp]: "0 < 1" begin

subclass semiring_1 ..
subclass comm_ring_1 ..
subclass ordered_ring ..
subclass ordered_comm_semiring by(unfold_locales, fact mult_left_mono)
subclass ordered_ab_semigroup_add ..

lemma of_nat_ge_0[simp]: "of_nat x ≥ 0"
proof (induct x)
  case 0 thus ?case by auto
  next case (Suc x)
    hence "0 ≤ of_nat x" by auto
    also have "of_nat x < of_nat (Suc x)" by auto
    finally show ?case by auto
qed

lemma of_nat_eq_0[simp]: "of_nat x = 0 ⟷ x = 0"
proof(induct x,simp)
  case (Suc x)
    have "of_nat (Suc x) > 0" apply(rule le_less_trans[of _ "of_nat x"]) by auto
    thus ?case by auto
qed

lemma inj_of_nat: "inj (of_nat :: nat ⇒ 'a)"
proof(rule injI)
  fix x y show "of_nat x = of_nat y ⟹ x = y"
  proof (induct x arbitrary: y)
    case 0 thus ?case
      proof (induct y)
        case 0 thus ?case by auto
        next case (Suc y)
          hence "of_nat (Suc y) = 0" by auto
          hence "Suc y = 0" unfolding of_nat_eq_0 by auto
          hence False by auto
          thus ?case by auto
      qed
    next case (Suc x)
      thus ?case
      proof (induct y)
        case 0
          hence "of_nat (Suc x) = 0" by auto
          hence "Suc x = 0" unfolding of_nat_eq_0 by auto
          hence False by auto
          thus ?case by auto
        next case (Suc y) thus ?case by auto
      qed
  qed
qed

subclass ring_char_0 by(unfold_locales, fact inj_of_nat)

end

(*
instance linordered_idom ⊆ ordered_semiring_strict by (intro_classes,auto)
instance linordered_idom ⊆ ordered_idom by (intro_classes, auto)
*)

end

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Missing Permutations›

text ‹This theory provides some definitions and lemmas on permutations which we did not find in the 
  Isabelle distribution.›

theory Missing_Permutations
imports
  Missing_Ring
  "HOL-Library.Permutations"
begin

definition signof :: "(nat ⇒ nat) ⇒ 'a :: ring_1" where
  "signof p = (if sign p = 1 then 1 else - 1)"

lemma signof_id[simp]: "signof id = 1" "signof (λ x. x) = 1"
  unfolding signof_def sign_id id_def[symmetric] by auto

lemma signof_inv: "finite S ⟹ p permutes S ⟹ signof (Hilbert_Choice.inv p) = signof p"
  unfolding signof_def using sign_inverse permutation_permutes by metis

lemma signof_pm_one: "signof p ∈ {1, - 1}"
  unfolding signof_def by auto

lemma signof_compose: assumes "p permutes {0..<(n :: nat)}"
  and "q permutes {0 ..<(m :: nat)}"
  shows "signof (p o q) = signof p * signof q"
proof -
  from assms have pp: "permutation p" "permutation q"
    by (auto simp: permutation_permutes)
  show "signof (p o q) = signof p * signof q"
    unfolding signof_def sign_compose[OF pp] 
    by (auto simp: sign_def split: if_splits)
qed

lemma permutes_funcset: "p permutes A ⟹ (p ` A → B) = (A → B)"
  by (simp add: permutes_image)

context comm_monoid
begin
lemma finprod_permute:
  assumes p: "p permutes S"
  and f: "f ∈ S → carrier G"
  shows "finprod G f S = finprod G (f ∘ p) S"
proof -
  from ‹p permutes S› have "inj p"
    by (rule permutes_inj)
  then have "inj_on p S"
    by (auto intro: subset_inj_on)
  from finprod_reindex[OF _ this, unfolded permutes_image[OF p], OF f]
  show ?thesis unfolding o_def .
qed

lemma finprod_singleton_set[simp]: assumes "f a ∈ carrier G"
  shows "finprod G f {a} = f a"
proof -
  have "finprod G f {a} = f a ⊗ finprod G f {}"
    by (rule finprod_insert, insert assms, auto)
  also have "… = f a" using assms by auto
  finally show ?thesis .
qed
end

lemmas (in semiring) finsum_permute = add.finprod_permute
lemmas (in semiring) finsum_singleton_set = add.finprod_singleton_set

lemma permutes_less[simp]: assumes p: "p permutes {0..<(n :: nat)}"
  shows "i < n ⟹ p i < n" "i < n ⟹ Hilbert_Choice.inv p i < n" 
  "p (Hilbert_Choice.inv p i) = i"
  "Hilbert_Choice.inv p (p i) = i"
proof -
  assume i: "i < n"
  show "p i < n" using permutes_in_image[OF p] i by auto
  let ?inv = "Hilbert_Choice.inv p" 
  have "⋀n. ?inv (p n) = n"
      using permutes_inverses[OF p] by simp
  thus "?inv i < n" 
      by (metis (no_types) atLeastLessThan_iff f_inv_into_f inv_into_into le0 permutes_image[OF p] i)
qed (insert permutes_inverses[OF p], auto)
    
context cring
begin

lemma finsum_permutations_inverse: 
  assumes f: "f ∈ {p. p permutes S} → carrier R"
  shows "finsum R f {p. p permutes S} = finsum R (λp. f(Hilbert_Choice.inv p)) {p. p permutes S}"
  (is "?lhs = ?rhs")
proof -
  let ?inv = "Hilbert_Choice.inv"
  let ?S = "{p . p permutes S}"
  have th0: "inj_on ?inv ?S"
  proof (auto simp add: inj_on_def)
    fix q r
    assume q: "q permutes S"
      and r: "r permutes S"
      and qr: "?inv q = ?inv r"
    then have "?inv (?inv q) = ?inv (?inv r)"
      by simp
    with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
      by metis
  qed
  have th1: "?inv ` ?S = ?S"
    using image_inverse_permutations by blast
  have th2: "?rhs = finsum R (f ∘ ?inv) ?S"
    by (simp add: o_def)
  from finsum_reindex[OF _ th0, of f] show ?thesis unfolding th1 th2 using f .
qed

lemma finsum_permutations_compose_right: assumes q: "q permutes S"
  and *: "f ∈ {p. p permutes S} → carrier R"
  shows "finsum R f {p. p permutes S} = finsum R (λp. f(p ∘ q)) {p. p permutes S}"
  (is "?lhs = ?rhs")
proof -
  let ?S = "{p. p permutes S}"
  let ?inv = "Hilbert_Choice.inv"
  have th0: "?rhs = finsum R (f ∘ (λp. p ∘ q)) ?S"
    by (simp add: o_def)
  have th1: "inj_on (λp. p ∘ q) ?S"
  proof (auto simp add: inj_on_def)
    fix p r
    assume "p permutes S"
      and r: "r permutes S"
      and rp: "p ∘ q = r ∘ q"
    then have "p ∘ (q ∘ ?inv q) = r ∘ (q ∘ ?inv q)"
      by (simp add: o_assoc)
    with permutes_surj[OF q, unfolded surj_iff] show "p = r"
      by simp
  qed
  have th3: "(λp. p ∘ q) ` ?S = ?S"
    using image_compose_permutations_right[OF q] by auto
  from finsum_reindex[OF _ th1, of f]
  show ?thesis unfolding th0 th1 th3 using * .
qed

end

text ‹The following lemma is slightly generalized from Determinants.thy in HMA.›

lemma finite_bounded_functions:
  assumes fS: "finite S"
  shows "finite T ⟹ finite {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}"
proof (induct T rule: finite_induct)
  case empty
  have th: "{f. ∀i. f i = i} = {id}"
    by auto
  show ?case
    by (auto simp add: th)
next
  case (insert a T)
  let ?f = "λ(y,g) i. if i = a then y else g i"
  let ?S = "?f ` (S × {f. (∀i∈T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)})"
  have "?S = {f. (∀i∈ insert a T. f i ∈ S) ∧ (∀i. i ∉ insert a T ⟶ f i = i)}"
    apply (auto simp add: image_iff)
    apply (rule_tac x="x a" in bexI)
    apply (rule_tac x = "λi. if i = a then i else x i" in exI)
    apply (insert insert, auto)
    done
  with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
  show ?case
    by metis
qed

lemma finite_bounded_functions':
  assumes fS: "finite S"
  shows "finite T ⟹ finite {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = j)}"
proof (induct T rule: finite_induct)
  case empty
  have th: "{f. ∀i. f i = j} = {(λ x. j)}"
    by auto
  show ?case
    by (auto simp add: th)
next
  case (insert a T)
  let ?f = "λ(y,g) i. if i = a then y else g i"
  let ?S = "?f ` (S × {f. (∀i∈T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = j)})"
  have "?S = {f. (∀i∈ insert a T. f i ∈ S) ∧ (∀i. i ∉ insert a T ⟶ f i = j)}"
    apply (auto simp add: image_iff)
    apply (rule_tac x="x a" in bexI)
    apply (rule_tac x = "λi. if i = a then j else x i" in exI)
    apply (insert insert, auto)
    done
  with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
  show ?case
    by metis
qed

context
  fixes A :: "'a set" 
    and B :: "'b set"
    and a_to_b :: "'a ⇒ 'b"
    and b_to_a :: "'b ⇒ 'a"
  assumes ab: "⋀ a. a ∈ A ⟹ a_to_b a ∈ B"
    and ba: "⋀ b. b ∈ B ⟹ b_to_a b ∈ A"
    and ab_ba: "⋀ a. a ∈ A ⟹ b_to_a (a_to_b a) = a"
    and ba_ab: "⋀ b. b ∈ B ⟹ a_to_b (b_to_a b) = b"
begin

qualified lemma permutes_memb: fixes p :: "'b ⇒ 'b"
  assumes p: "p permutes B"
  and a: "a ∈ A"
  defines "ip ≡ Hilbert_Choice.inv p"
  shows "a ∈ A" "a_to_b a ∈ B" "ip (a_to_b a) ∈ B" "p (a_to_b a) ∈ B" 
    "b_to_a (p (a_to_b a)) ∈ A" "b_to_a (ip (a_to_b a)) ∈ A"
proof -
  let ?b = "a_to_b a"
  from p have ip: "ip permutes B" unfolding ip_def by (rule permutes_inv)
  note in_ip = permutes_in_image[OF ip]
  note in_p = permutes_in_image[OF p]
  show a: "a ∈ A" by fact
  show b: "?b ∈ B" by (rule ab[OF a])
  show pb: "p ?b ∈ B" unfolding in_p by (rule b)
  show ipb: "ip ?b ∈ B" unfolding in_ip by (rule b)
  show "b_to_a (p ?b) ∈ A" by (rule ba[OF pb])
  show "b_to_a (ip ?b) ∈ A" by (rule ba[OF ipb])
qed

lemma permutes_bij_main: 
  "{p . p permutes A} ⊇ (λ p a. if a ∈ A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}" 
  (is "?A ⊇ ?f ` ?B")
proof 
  note d = permutes_def
  let ?g = "λ q b. if b ∈ B then a_to_b (q (b_to_a b)) else b"
  let ?inv = "Hilbert_Choice.inv"
  fix p
  assume p: "p ∈ ?f ` ?B"
  then obtain q where q: "q permutes B" and p: "p = ?f q" by auto    
  let ?iq = "?inv q"
  from q have iq: "?iq permutes B" by (rule permutes_inv)
  note in_iq = permutes_in_image[OF iq]
  note in_q = permutes_in_image[OF q]
  have qiB: "⋀ b. b ∈ B ⟹ q (?iq b) = b" using q by (rule permutes_inverses)
  have iqB: "⋀ b. b ∈ B ⟹ ?iq (q b) = b" using q by (rule permutes_inverses)
  from q[unfolded d] 
  have q1: "⋀ b. b ∉ B ⟹ q b = b" 
   and q2: "⋀ b. ∃!b'. q b' = b" by auto
  note memb = permutes_memb[OF q]
  show "p ∈ ?A" unfolding p d
  proof (rule, intro conjI impI allI, force)
    fix a
    show "∃!a'. ?f q a' = a"
    proof (cases "a ∈ A")
      case True
      note a = memb[OF True]
      let ?a = "b_to_a (?iq (a_to_b a))"
      show ?thesis
      proof 
        show "?f q ?a = a" using a by (simp add: ba_ab qiB ab_ba)
      next
        fix a'
        assume id: "?f q a' = a"
        show "a' = ?a"
        proof (cases "a' ∈ A")
          case False
          thus ?thesis using id a by auto
        next
          case True
          note a' = memb[OF this]
          from id True have "b_to_a (q (a_to_b a')) = a" by simp
          from arg_cong[OF this, of "a_to_b"] a' a
          have "q (a_to_b a') = a_to_b a" by (simp add: ba_ab)
          from arg_cong[OF this, of ?iq]
          have "a_to_b a' = ?iq (a_to_b a)" unfolding iqB[OF a'(2)] .
          from arg_cong[OF this, of b_to_a] show ?thesis unfolding ab_ba[OF True] .
        qed
      qed
    next
      case False note a = this
      show ?thesis
      proof
        show "?f q a = a" using a by simp
      next
        fix a'
        assume id: "?f q a' = a"
        show "a' = a"
        proof (cases "a' ∈ A")
          case False
          with id show ?thesis by simp
        next
          case True
          note a' = memb[OF True]
          with id False show ?thesis by auto
        qed
      qed
    qed
  qed
qed
end

lemma  permutes_bij': assumes ab: "⋀ a. a ∈ A ⟹ a_to_b a ∈ B"
    and ba: "⋀ b. b ∈ B ⟹ b_to_a b ∈ A"
    and ab_ba: "⋀ a. a ∈ A ⟹ b_to_a (a_to_b a) = a"
    and ba_ab: "⋀ b. b ∈ B ⟹ a_to_b (b_to_a b) = b"
  shows "{p . p permutes A} = (λ p a. if a ∈ A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}" 
  (is "?A = ?f ` ?B")
proof -
  note one_dir = ab ba ab_ba ba_ab
  note other_dir = ba ab ba_ab ab_ba
  let ?g = "(λ p b. if b ∈ B then a_to_b (p (b_to_a b)) else b)"
  define PA where "PA = ?A"
  define f where "f = ?f"
  define g where "g = ?g"
  {
    fix p
    assume "p ∈ PA"
    hence p: "p permutes A" unfolding PA_def by simp
    from p[unfolded permutes_def] have pnA: "⋀ a. a ∉ A ⟹ p a = a" by auto
    have "?f (?g p) = p"
    proof (rule ext)
      fix a
      show "?f (?g p) a = p a"
      proof (cases "a ∈ A")
        case False
        thus ?thesis by (simp add: pnA)
      next
        case True note a = this
        hence "p a ∈ A" unfolding permutes_in_image[OF p] .
        thus ?thesis using a by (simp add: ab_ba ba_ab ab)
      qed
    qed
    hence "f (g p) = p" unfolding f_def g_def .
  }
  hence "f ` g ` PA = PA" by force
  hence id: "?f ` ?g ` ?A = ?A" unfolding PA_def f_def g_def .
  have "?f ` ?B ⊆ ?A" by (rule permutes_bij_main[OF one_dir])
  moreover have "?g ` ?A ⊆ ?B" by (rule permutes_bij_main[OF ba ab ba_ab ab_ba])
  hence "?f ` ?g ` ?A ⊆ ?f ` ?B" by auto
  hence "?A ⊆ ?f ` ?B" unfolding id .
  ultimately show ?thesis by blast
qed    

lemma inj_on_nat_permutes: assumes i: "inj_on f (S :: nat set)"
  and fS: "f ∈ S → S"
  and fin: "finite S"
  and f: "⋀ i. i ∉ S ⟹ f i = i"
  shows "f permutes S"
  unfolding permutes_def
proof (intro conjI allI impI, rule f)
  fix y
  from endo_inj_surj[OF fin _ i] fS have fs: "f ` S = S" by auto
  show "∃!x. f x = y"
  proof (cases "y ∈ S")
    case False
    thus ?thesis by (intro ex1I[of _ y], insert fS f, auto)
  next
    case True
    with fs obtain x where x: "x ∈ S" and fx: "f x = y" by force
    show ?thesis
    proof (rule ex1I, rule fx)
      fix x'
      assume fx': "f x' = y"
      with True f[of x'] have "x' ∈ S" by metis
      from inj_onD[OF i fx[folded fx'] x this]
      show "x' = x" by simp
    qed
  qed
qed


lemma permutes_pair_eq:
  assumes p: "p permutes S"
  shows "{ (p s, s) | s. s ∈ S } = { (s, Hilbert_Choice.inv p s) | s. s ∈ S }"
    (is "?L = ?R")
proof
  show "?L ⊆ ?R"
  proof
    fix x assume "x ∈ ?L"
    then obtain s where x: "x = (p s, s)" and s: "s ∈ S" by auto
    note x
    also have "(p s, s) = (p s, Hilbert_Choice.inv p (p s))"
      using permutes_inj[OF p] inv_f_f by auto
    also have "... ∈ ?R" using s permutes_in_image[OF p] by auto
    finally show "x ∈ ?R".
  qed
  show "?R ⊆ ?L"
  proof
    fix x assume "x ∈ ?R"
    then obtain s
      where x: "x = (s, Hilbert_Choice.inv p s)" (is "_ = (s, ?ips)")
        and s: "s ∈ S" by auto
    note x
    also have "(s, ?ips) = (p ?ips, ?ips)"
      using inv_f_f[OF permutes_inj[OF permutes_inv[OF p]]]
      using inv_inv_eq[OF permutes_bij[OF p]] by auto
    also have "... ∈ ?L"
      using s permutes_in_image[OF permutes_inv[OF p]] by auto
    finally show "x ∈ ?L".
  qed
qed

lemma inj_on_finite[simp]:
  assumes inj: "inj_on f A" shows "finite (f ` A) = finite A"
proof
  assume fin: "finite (f ` A)"
  show "finite A"
  proof (cases "card (f ` A) = 0")
    case True thus ?thesis using fin by auto
    next case False 
      hence "card A > 0" unfolding card_image[OF inj] by auto
      thus ?thesis using card.infinite by force
  qed
qed auto

lemma permutes_prod:
  assumes p: "p permutes S"
  shows "(∏s∈S. f (p s) s) = (∏s∈S. f s (Hilbert_Choice.inv p s))"
    (is "?l = ?r")
proof -
  let ?f = "λ(x,y). f x y"
  let ?ps = "λs. (p s, s)"
  let ?ips = "λs. (s, Hilbert_Choice.inv p s)"
  have inj1: "inj_on ?ps S" by (rule inj_onI;auto)
  have inj2: "inj_on ?ips S" by (rule inj_onI;auto)
  have "?l = prod ?f (?ps ` S)"
    using prod.reindex[OF inj1, of ?f] by simp
  also have "?ps ` S = {(p s, s) |s. s ∈ S}" by auto
  also have "... = {(s, Hilbert_Choice.inv p s) | s. s ∈ S}"
    unfolding permutes_pair_eq[OF p] by simp
  also have "... = ?ips ` S" by auto
  also have "prod ?f ... = ?r"
    using prod.reindex[OF inj2, of ?f] by simp
  finally show ?thesis.
qed

lemma permutes_sum:
  assumes p: "p permutes S"
  shows "(∑s∈S. f (p s) s) = (∑s∈S. f s (Hilbert_Choice.inv p s))"
    (is "?l = ?r")
proof -
  let ?f = "λ(x,y). f x y"
  let ?ps = "λs. (p s, s)"
  let ?ips = "λs. (s, Hilbert_Choice.inv p s)"
  have inj1: "inj_on ?ps S" by (rule inj_onI;auto)
  have inj2: "inj_on ?ips S" by (rule inj_onI;auto)
  have "?l = sum ?f (?ps ` S)"
    using sum.reindex[OF inj1, of ?f] by simp
  also have "?ps ` S = {(p s, s) |s. s ∈ S}" by auto
  also have "... = {(s, Hilbert_Choice.inv p s) | s. s ∈ S}"
    unfolding permutes_pair_eq[OF p] by simp
  also have "... = ?ips ` S" by auto
  also have "sum ?f ... = ?r"
    using sum.reindex[OF inj2, of ?f] by simp
  finally show ?thesis.
qed

lemma inv_inj_on_permutes: "inj_on Hilbert_Choice.inv { p. p permutes S }"
proof (intro inj_onI, unfold mem_Collect_eq)
  let ?i = "Hilbert_Choice.inv"
  fix p q
  assume p: "p permutes S" and q: "q permutes S" and eq: "?i p = ?i q"
  have "?i (?i p) = ?i (?i q)" using eq by simp
  thus "p = q"
    using inv_inv_eq[OF permutes_bij] p q by metis
qed

lemma permutes_others:
  assumes p: "p permutes S" and x: "x ∉ S" shows "p x = x"
  using p unfolding permutes_def using x by simp

end

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
theory Conjugate
  imports HOL.Complex
begin

class conjugate =
  fixes conjugate :: "'a ⇒ 'a"
  assumes conjugate_id[simp]: "conjugate (conjugate a) = a"
      and conjugate_cancel_iff[simp]: "conjugate a = conjugate b ⟷ a = b"

class conjugatable_ring = ring + conjugate +
  assumes conjugate_dist_mul: "conjugate (a * b) = conjugate a * conjugate b"
      and conjugate_dist_add: "conjugate (a + b) = conjugate a + conjugate b"
      and conjugate_neg: "conjugate (-a) = - conjugate a"
      and conjugate_zero[simp]: "conjugate 0 = 0"
begin
  lemma conjugate_zero_iff[simp]: "conjugate a = 0 ⟷ a = 0"
    using conjugate_cancel_iff[of _ 0, unfolded conjugate_zero].
end

class conjugatable_field = conjugatable_ring + field

lemma sum_conjugate:
  fixes f :: "'b ⇒ 'a :: conjugatable_ring"
  assumes finX: "finite X"
  shows "conjugate (sum f X) = sum (λx. conjugate (f x)) X"
  using finX by (induct set:finite, auto simp: conjugate_dist_add)

class conjugatable_ordered_ring = conjugatable_ring + ordered_comm_monoid_add +
  assumes conjugate_square_positive: "a * conjugate a ≥ 0"

class conjugatable_ordered_field = conjugatable_ordered_ring + field
begin
  subclass conjugatable_field..
end

lemma conjugate_square_0:
  fixes a :: "'a :: {conjugatable_ordered_ring, semiring_no_zero_divisors}"
  shows "a * conjugate a = 0 ⟹ a = 0" by auto


subsection ‹Instantiations›

instantiation complex :: conjugatable_ordered_field
begin
  definition [simp]: "conjugate ≡ cnj"
  definition [simp]: "x < y ≡ Im x = Im y ∧ Re x < Re y"
  definition [simp]: "x ≤ y ≡ Im x = Im y ∧ Re x ≤ Re y"
  
  instance by (intro_classes, auto simp: complex.expand)
end

instantiation real :: conjugatable_ordered_field
begin
  definition [simp]: "conjugate (x::real) ≡ x"
  instance by (intro_classes, auto)
end

instantiation rat :: conjugatable_ordered_field
begin
  definition [simp]: "conjugate (x::rat) ≡ x"
  instance by (intro_classes, auto)
end

instantiation int :: conjugatable_ordered_ring
begin
  definition [simp]: "conjugate (x::int) ≡ x"
  instance by (intro_classes, auto)
end

lemma conjugate_square_eq_0 [simp]:
  fixes x :: "'a :: {conjugatable_ring,semiring_no_zero_divisors}"
  shows "x * conjugate x = 0 ⟷ x = 0" "conjugate x * x = 0 ⟷ x = 0"
  by auto

lemma conjugate_square_greater_0 [simp]:
  fixes x :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors}"
  shows "x * conjugate x > 0 ⟷ x ≠ 0" 
  using conjugate_square_positive[of x]
  by (auto simp: le_less)

lemma conjugate_square_smaller_0 [simp]:
  fixes x :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors}"
  shows "¬ x * conjugate x < 0"
  using conjugate_square_positive[of x] by auto

end